=============================
Step 1

? (all x ((inv (inv x)) = x))


> revsk
=============================
Step 2

? ((inv (inv c22493)) = c22493)


> hypdisj
=============================
Step 3

? ((inv (inv c22493)) = c22493)


> rewriteB (inv (inv c22493))
|=============================
|Step 4
|
|? ((+ e (inv (inv c22493))) = (inv (inv c22493)))
|
|
|> (((+ e X) = X) <--)
=============================
Step 5

? ((+ e (inv (inv c22493))) = c22493)


> rewriteB e
|=============================
|Step 6
|
|? ((+ Var77 (inv Var77)) = e)
|
|
|> (((+ X (inv X)) = e) <--)
=============================
Step 7

? ((+ (+ c22493 (inv c22493)) (inv (inv c22493))) = c22493)


> rewriteB (+ (+ c22493 (inv c22493)) (inv (inv c22493)))
|=============================
|Step 8
|
|? ((+ c22493 (+ (inv c22493) (inv (inv c22493)))) = (+ (+ c22493 (inv c22493)) (inv (inv c22493))))
|
|
|> (((+ X (+ Y Z)) = (+ (+ X Y) Z)) <--)
=============================
Step 9

? ((+ c22493 (+ (inv c22493) (inv (inv c22493)))) = c22493)


> rewriteA (+ (inv c22493) (inv (inv c22493)))
|=============================
|Step 10
|
|? ((+ (inv c22493) (inv (inv c22493))) = e)
|
|
|> (((+ X (inv X)) = e) <--)
=============================
Step 11

? ((+ c22493 e) = c22493)


> (((+ X e) = X) <--)
